Skip to content

Adding support for Machine Integer version of Bytes, List, and MInt functions #1209

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 16 commits into from
Jul 14, 2025

Conversation

Robertorosmaninho
Copy link
Collaborator

@Robertorosmaninho Robertorosmaninho commented Jun 28, 2025

This PR introduces the concrete implementation of the following new Machine Integer hooks:

1.  syntax {Width} MInt{Width} ::=MInt{Width} "^MInt" MInt{Width}
2.  syntax {Width} Bytes ::= MInt2Bytes(MInt{Width})
3.  syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes)
4.  syntax {Width} MInt{Width} ::= lengthBytes(Bytes)
5.  syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width})
6.  syntax {Width} Bytes ::= padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width})
7.  syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes)
8.  syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width})
9.  syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]"
10. syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]"
11. syntax {Width} MInt{Width} ::= size(List)
12. syntax {Width} List ::= List "[" index: MInt{Width} "<-" value: KItem "]"
13. syntax {Width} KItem ::= List "[" MInt{Width} "]"

Most of these hooks have an initial implementation for 64 and 256-bit Integers, being the former defined in C++ in its respective collection file while the latter is defined in the llvm_header.inc file, as C++ doesn't support 256-bit integer natively.

The only exceptions for now are 12 and 13, which are only implemented for 64-bit, as we have the immer limitation that the index should be a in64_t.

@rv-jenkins rv-jenkins changed the base branch from master to develop June 28, 2025 17:17
…d MInt{64}

Implementing `hook_MINT_pow256` in LLVM IR
Implementing `hook_MINT_pow64` in int.cpp
Adding `mint-pow` unit test
Implementing `hook_MINT_MInt2Bytes` in LLVM IR
Adding `mint2bytes` unit test
Implementing `hook_MINT_Bytes2MInt` in LLVM IR
Adding `bytes2mint` unit test
…} and MInt{64}

Implementing `hook_BYTES_length256` in LLVM IR
Implementing `hook_BYTES_length64` in bytes.cpp
Adding `lengthbytes` unit test
…56} and MInt{64}

Implementing `hook_BYTES_padRight256` in LLVM IR
Implementing `hook_BYTES_padRight64` in bytes.cpp
Adding `padrightbytes` unit test
…6} and MInt{64}

Implementing `hook_BYTES_padLeft256` in LLVM IR
Implementing `hook_BYTES_padLeft64` in bytes.cpp
Adding `padleftbytes` unit test
…256} and MInt{64}

Implementing `hook_BYTES_replaceAt256` in LLVM IR
Implementing `hook_BYTES_replaceAt64` in bytes.cpp
Adding `replaceatbytes` unit test
Declaring functions needed by other functions in the `llvm_hearder.inc`
Defining `interger_overflow` used in used in `hook_BYTES_pad*` functions in `llvm_hearder.inc`
…} and MInt{64}

Implementing `hook_BYTES_substr256` in LLVM IR
Implementing `hook_BYTES_substr64` in bytes.cpp
Adding `substrbytes` unit test
…nd MInt{64}

Implementing `hook_BYTES_get256` in LLVM IR
Implementing `hook_BYTES_get64` in bytes.cpp
Adding `bytes-get` unit test
…} and MInt{64}

Implementing `hook_BYTES_update256` in LLVM IR
Implementing `hook_BYTES_update64` in bytes.cpp
Adding `bytes-update` unit test
…nd MInt{64}

Implementing `hook_LIST_size256` in LLVM IR
Implementing `hook_LIST_size64` in bytes.cpp
Adding `list-size` unit test
Implementing `hook_LIST_get64` in bytes.cpp
Adding `list-get` unit test
@Robertorosmaninho Robertorosmaninho self-assigned this Jul 4, 2025
@Robertorosmaninho Robertorosmaninho marked this pull request as ready for review July 4, 2025 19:38
Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd suggest considering the following two factors regarding the hooks added:

  1. Is there a particularly compelling reason why both arguments of hooks with more than one mint arg need to have the same size?
  2. If a mint arg or return value carresponds to a size in bytes or in elements of something in memory, you should be able to use a non parametric mint 64 for it.

None of this is absolutely necessary but if we're adding hooks to the frontend we ought to think about this.

@@ -111,6 +120,10 @@ size_t hook_LIST_size_long(SortList list) {
return list->size();
}

uint64_t hook_LIST_size64(SortList list) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hook_list_size_long already does this. Check for other similar duplicates that may exist.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But it can return a 32-bit in 32-bit machines, right? As in CreateTerm.cpp, we set this return type fixed in i64; wouldn't it be better to be sure we're always returning the correct type?

@Robertorosmaninho
Copy link
Collaborator Author

Robertorosmaninho commented Jul 8, 2025

Is there a particularly compelling reason why both arguments of hooks with more than one mint arg need to have the same size?

Not necessarily, but that's how we defined it in the frontend. We also haven't reached the need to use 2 different bit sizes as well.

If a mint arg or return value corresponds to a size in bytes or in elements of something in memory, you should be able to use a non parametric mint 64 for it.

I agree, and it makes sense, but it will enforce a roundMInt to users of this function if they're using a type different from i64, right? In our case, we're mainly using i256 in EVM, so if we enforce an i64 here, we'll have to delegate the responsibility to truncate the integer to the user instead of the function. My initial idea was to delegate this responsibility to the function to make the interface nicer. What do you think?

Also, @dwightguth, do you have any comments on how I can have:

  1. A List return type in CreateTerm.cpp; and
  2. How is the correct way to handle the list data type in LLVM IR, so we can have i256 versions of the List hooks there as well?

@Robertorosmaninho Robertorosmaninho requested a review from theo25 July 10, 2025 15:19
Copy link
Collaborator

@mariaKt mariaKt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you @Robertorosmaninho. I added only two minor comments.

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit bb5318b into develop Jul 14, 2025
10 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the mint64-hooks branch July 14, 2025 19:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants